2020-0727-SYMCC
会议：USENIX’20
论文名称：Symbolic execution with SYMCC: Don’t interpret, compile!
Introduction
作者认为目前的符号执行技术的一大缺陷是速度很慢，因此作者提出了基于编译器的混合符号执行技术。将构造约束的代码在编译时嵌入到程序当中，在运行时进行符号执行及约束求解，从而提高符号执行的速度。作者使用SYMCC发现了OpenJPEG中的两个漏洞。
开源代码：http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
Background
目前常见的符号执行分为两类：IR-based、IR-less
IR-based symbolic execution
将binary提升到IR，再进行抽象解释。一大缺陷是容易路径爆炸
常见的有KLEE、Mayhem、angr
IR-less symbolic execution
混合执行（concolic execution），通过动态插桩技术，tracing native execution while inserting bits of code，执行部分指令后再构造符号表达式。优点是快，缺点是injected analysis code可能无法生成正确的符号表达式，且较依赖于指令集。
常见的有：Triton、QSYM、SAGE、Driller
Reducing overhead
concreteness checks: A common optimization strategy is therefore to restrict symbolic handling to computations on symbolic data and resort to a faster execution mechanism otherwise.
Compilation-based symbolic execution
overview
插桩前后的example:
Support library
Listing 2中的函数调用为library中的API。
Symbolic handlers
Listing 2中，似乎就是根据IR，插入了数次API调用，将表达式符号化。
Implementation
Compile-time instrumentation
作者在IR阶段进行插桩，在优化中间进行插桩（dead-code elimination and strength reduction之后，vectorizer (i.e., the stage that replaces loops with SIMD instructions on supported architectures)之前）。
作者对LLVM IR进行抽象解释，类似于IR-based symbolic interpreters（KLEE、S2E），但由于仅需要遍历一遍，不需要重复的遍历，因此编译时插桩的开销较低。
Concreteness checks
（留个坑，还是有点不太理解Concreteness checks检查操作数是concrete还是symbolic的细节
Before each computation in the bitcode, we insert a conditional jump that skips symbolic handling altogether if all operands are concrete; if at least one operand is symbolic, we create the symbolic expressions for the other operands as needed and call out to the symbolic backend.
Evaluation
Pure execution time
Execution time with symbolic inputs
Coverage
Others
局限性：source base，文末讨论时说可以利用某些工具将binary提升到LLVM IR再继续插桩，但这样会使得开销急剧上升。
一些疑点：
- 速度和覆盖率比其他的符号执行工具更快的原因：
- 只看给的example，发现其仅是对各种LLVM IR进行解析，调用后端的一个函数进行处理
- 所以本质上来说，SYMCC是一款source-based符号执行工具
- 实验是与binary-based的符号执行工具进行对比
测试了一下：
不知道是不是case的问题，测试的效果很差，只有当字符串长度相同时才能够成功求出约束，不同长度字符串作为输入及int都无法solve。
左右为源码及生成的IR
